Added a README describing the Heapster implication rules #1554
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
eddywestbrook
added
subsystem: heapster
jpaykin
approved these changes
Jan 11, 2022
|
|
||
| The main logic for proving most of the permission constructs is in the next function down, `proveVarImplInt`, which proves a single permission on a variable `x`. It does this by first pushing the primary permsisions `p` for `x` onto the top of the stack and then proving an implication `x:p |- x:mb_p`, where `mb_p` is the desired permission that we want to prove for `x`. The "mb" prefix indicates that `mb_p` is a permission inside a multi-binding, i.e., a binding of 0 or more existential variables that could be used in the permission we are trying to prove. The `proveVarImplInt` then proceeds by case analysis on `p` and `mb_p`, in most cases using either an introduction rule for proving a construct in `mb_p` on the right or an elimination rule for eliminating a construct in `p` on the left combined with a recursive call to `proveVarImplInt` to prove the remaining implication for smaller `p` and/or smaller `mb_p`. The most complex cases are for proving an equality permission on the right or for proving an implication `x:p1 * ... * pn |- x:p1' * ... * pm'` between conjuncts permissions. For an equality permission on the right, the special-purpose helper function `proveVarEq` is used to prove equality permissions `x:eq(e)` based on the structure of `e`. For proving an implication of conjuncts, the function `proveVarConjImpl` is used, which is structured in a similar manner to `proveVarsImplAppendInt`, in that it repeatedly chooses the "best" permission on the right to prove, proves it, and then recursively proves the remaining permissions on the right until they have all been proved. | ||
|
|
||
| The `proveVarAtomicImpl` function is called by `proveVarConjImpl` to prove each conjunct. This function performs |
There was a problem hiding this comment.
This and the next few paragraphs have cut-off sentences. It's fine that this is work in progress, I would just remove the sentence fragments an put TODO's or FIXME's there if you need to remember that spot.
There was a problem hiding this comment.
Whoops, you're right! Need to fix that...
eddywestbrook
removed
the
PR: ready to merge
added 19 commits
January 17, 2022 15:51
…ype, with FIXMEs for the explanations
…n to correctly handle slices
eddywestbrook
added
the
PR: ready to merge
|
This now includes documentation about the Rust-to-Heapster translation, which is a useful way to help understand the Heapster type system |
eddywestbrook
removed
the
PR: ready to merge
eddywestbrook
added
the
PR: ready to merge
m-yac
approved these changes
Jun 14, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.